Nuprl Lemma : first0
0,22
postcript
pdf
L
:Top List. firstn(0;
L
) ~ nil
latex
Definitions
i
<
j
,
firstn(
n
;
as
)
,
x
:
A
.
B
(
x
)
,
Top
origin
L:Top List. firstn(0;L) ~ nil L:Top List. firstn(0;L) ~ nil 
jx:A. B(x)